0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 170 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 178 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇔, 15 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇔, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 PiDP
↳22 PiDPToQDPProof (⇒, 0 ms)
↳23 QDP
↳24 MRRProof (⇔, 206 ms)
↳25 QDP
↳26 DependencyGraphProof (⇔, 0 ms)
↳27 TRUE
MERGEA_IN_GGA(.(0, X1), .(0, X2), .(0, X3)) → U3_GGA(X1, X2, X3, mergeA_in_gga(X1, .(0, X2), X3))
MERGEA_IN_GGA(.(0, X1), .(0, X2), .(0, X3)) → MERGEA_IN_GGA(X1, .(0, X2), X3)
MERGEA_IN_GGA(.(0, X1), .(s(0), X2), .(0, X3)) → U4_GGA(X1, X2, X3, mergeA_in_gga(X1, .(s(0), X2), X3))
MERGEA_IN_GGA(.(0, X1), .(s(0), X2), .(0, X3)) → MERGEA_IN_GGA(X1, .(s(0), X2), X3)
MERGEA_IN_GGA(.(s(X1), X2), .(s(X3), X4), .(s(X1), X5)) → U5_GGA(X1, X2, X3, X4, X5, leqB_in_gg(X1, X3))
MERGEA_IN_GGA(.(s(X1), X2), .(s(X3), X4), .(s(X1), X5)) → LEQB_IN_GG(X1, X3)
LEQB_IN_GG(s(X1), s(X2)) → U1_GG(X1, X2, leqB_in_gg(X1, X2))
LEQB_IN_GG(s(X1), s(X2)) → LEQB_IN_GG(X1, X2)
MERGEA_IN_GGA(.(s(X1), X2), .(s(X3), X4), .(s(X1), X5)) → U6_GGA(X1, X2, X3, X4, X5, leqcB_in_gg(X1, X3))
U6_GGA(X1, X2, X3, X4, X5, leqcB_out_gg(X1, X3)) → U7_GGA(X1, X2, X3, X4, X5, mergeA_in_gga(X2, .(s(X3), X4), X5))
U6_GGA(X1, X2, X3, X4, X5, leqcB_out_gg(X1, X3)) → MERGEA_IN_GGA(X2, .(s(X3), X4), X5)
MERGEA_IN_GGA(.(X1, X2), .(X3, X4), .(X3, X5)) → U8_GGA(X1, X2, X3, X4, X5, lessC_in_gg(X3, X1))
MERGEA_IN_GGA(.(X1, X2), .(X3, X4), .(X3, X5)) → LESSC_IN_GG(X3, X1)
LESSC_IN_GG(s(X1), s(X2)) → U2_GG(X1, X2, lessC_in_gg(X1, X2))
LESSC_IN_GG(s(X1), s(X2)) → LESSC_IN_GG(X1, X2)
MERGEA_IN_GGA(.(X1, X2), .(X3, X4), .(X3, X5)) → U9_GGA(X1, X2, X3, X4, X5, lesscC_in_gg(X3, X1))
U9_GGA(X1, X2, X3, X4, X5, lesscC_out_gg(X3, X1)) → U10_GGA(X1, X2, X3, X4, X5, mergeA_in_gga(.(X1, X2), X4, X5))
U9_GGA(X1, X2, X3, X4, X5, lesscC_out_gg(X3, X1)) → MERGEA_IN_GGA(.(X1, X2), X4, X5)
MERGEA_IN_GGA(.(s(0), X1), .(0, X2), .(0, X3)) → U11_GGA(X1, X2, X3, mergeA_in_gga(.(s(0), X1), X2, X3))
MERGEA_IN_GGA(.(s(0), X1), .(0, X2), .(0, X3)) → MERGEA_IN_GGA(.(s(0), X1), X2, X3)
MERGEA_IN_GGA(.(s(X1), X2), .(s(X3), X4), .(s(X3), X5)) → U12_GGA(X1, X2, X3, X4, X5, lessC_in_gg(X3, X1))
MERGEA_IN_GGA(.(s(X1), X2), .(s(X3), X4), .(s(X3), X5)) → LESSC_IN_GG(X3, X1)
MERGEA_IN_GGA(.(s(X1), X2), .(s(X3), X4), .(s(X3), X5)) → U13_GGA(X1, X2, X3, X4, X5, lesscC_in_gg(X3, X1))
U13_GGA(X1, X2, X3, X4, X5, lesscC_out_gg(X3, X1)) → U14_GGA(X1, X2, X3, X4, X5, mergeA_in_gga(.(s(X1), X2), X4, X5))
U13_GGA(X1, X2, X3, X4, X5, lesscC_out_gg(X3, X1)) → MERGEA_IN_GGA(.(s(X1), X2), X4, X5)
leqcB_in_gg(0, 0) → leqcB_out_gg(0, 0)
leqcB_in_gg(0, s(0)) → leqcB_out_gg(0, s(0))
leqcB_in_gg(s(X1), s(X2)) → U25_gg(X1, X2, leqcB_in_gg(X1, X2))
U25_gg(X1, X2, leqcB_out_gg(X1, X2)) → leqcB_out_gg(s(X1), s(X2))
lesscC_in_gg(0, s(0)) → lesscC_out_gg(0, s(0))
lesscC_in_gg(s(X1), s(X2)) → U26_gg(X1, X2, lesscC_in_gg(X1, X2))
U26_gg(X1, X2, lesscC_out_gg(X1, X2)) → lesscC_out_gg(s(X1), s(X2))
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
MERGEA_IN_GGA(.(0, X1), .(0, X2), .(0, X3)) → U3_GGA(X1, X2, X3, mergeA_in_gga(X1, .(0, X2), X3))
MERGEA_IN_GGA(.(0, X1), .(0, X2), .(0, X3)) → MERGEA_IN_GGA(X1, .(0, X2), X3)
MERGEA_IN_GGA(.(0, X1), .(s(0), X2), .(0, X3)) → U4_GGA(X1, X2, X3, mergeA_in_gga(X1, .(s(0), X2), X3))
MERGEA_IN_GGA(.(0, X1), .(s(0), X2), .(0, X3)) → MERGEA_IN_GGA(X1, .(s(0), X2), X3)
MERGEA_IN_GGA(.(s(X1), X2), .(s(X3), X4), .(s(X1), X5)) → U5_GGA(X1, X2, X3, X4, X5, leqB_in_gg(X1, X3))
MERGEA_IN_GGA(.(s(X1), X2), .(s(X3), X4), .(s(X1), X5)) → LEQB_IN_GG(X1, X3)
LEQB_IN_GG(s(X1), s(X2)) → U1_GG(X1, X2, leqB_in_gg(X1, X2))
LEQB_IN_GG(s(X1), s(X2)) → LEQB_IN_GG(X1, X2)
MERGEA_IN_GGA(.(s(X1), X2), .(s(X3), X4), .(s(X1), X5)) → U6_GGA(X1, X2, X3, X4, X5, leqcB_in_gg(X1, X3))
U6_GGA(X1, X2, X3, X4, X5, leqcB_out_gg(X1, X3)) → U7_GGA(X1, X2, X3, X4, X5, mergeA_in_gga(X2, .(s(X3), X4), X5))
U6_GGA(X1, X2, X3, X4, X5, leqcB_out_gg(X1, X3)) → MERGEA_IN_GGA(X2, .(s(X3), X4), X5)
MERGEA_IN_GGA(.(X1, X2), .(X3, X4), .(X3, X5)) → U8_GGA(X1, X2, X3, X4, X5, lessC_in_gg(X3, X1))
MERGEA_IN_GGA(.(X1, X2), .(X3, X4), .(X3, X5)) → LESSC_IN_GG(X3, X1)
LESSC_IN_GG(s(X1), s(X2)) → U2_GG(X1, X2, lessC_in_gg(X1, X2))
LESSC_IN_GG(s(X1), s(X2)) → LESSC_IN_GG(X1, X2)
MERGEA_IN_GGA(.(X1, X2), .(X3, X4), .(X3, X5)) → U9_GGA(X1, X2, X3, X4, X5, lesscC_in_gg(X3, X1))
U9_GGA(X1, X2, X3, X4, X5, lesscC_out_gg(X3, X1)) → U10_GGA(X1, X2, X3, X4, X5, mergeA_in_gga(.(X1, X2), X4, X5))
U9_GGA(X1, X2, X3, X4, X5, lesscC_out_gg(X3, X1)) → MERGEA_IN_GGA(.(X1, X2), X4, X5)
MERGEA_IN_GGA(.(s(0), X1), .(0, X2), .(0, X3)) → U11_GGA(X1, X2, X3, mergeA_in_gga(.(s(0), X1), X2, X3))
MERGEA_IN_GGA(.(s(0), X1), .(0, X2), .(0, X3)) → MERGEA_IN_GGA(.(s(0), X1), X2, X3)
MERGEA_IN_GGA(.(s(X1), X2), .(s(X3), X4), .(s(X3), X5)) → U12_GGA(X1, X2, X3, X4, X5, lessC_in_gg(X3, X1))
MERGEA_IN_GGA(.(s(X1), X2), .(s(X3), X4), .(s(X3), X5)) → LESSC_IN_GG(X3, X1)
MERGEA_IN_GGA(.(s(X1), X2), .(s(X3), X4), .(s(X3), X5)) → U13_GGA(X1, X2, X3, X4, X5, lesscC_in_gg(X3, X1))
U13_GGA(X1, X2, X3, X4, X5, lesscC_out_gg(X3, X1)) → U14_GGA(X1, X2, X3, X4, X5, mergeA_in_gga(.(s(X1), X2), X4, X5))
U13_GGA(X1, X2, X3, X4, X5, lesscC_out_gg(X3, X1)) → MERGEA_IN_GGA(.(s(X1), X2), X4, X5)
leqcB_in_gg(0, 0) → leqcB_out_gg(0, 0)
leqcB_in_gg(0, s(0)) → leqcB_out_gg(0, s(0))
leqcB_in_gg(s(X1), s(X2)) → U25_gg(X1, X2, leqcB_in_gg(X1, X2))
U25_gg(X1, X2, leqcB_out_gg(X1, X2)) → leqcB_out_gg(s(X1), s(X2))
lesscC_in_gg(0, s(0)) → lesscC_out_gg(0, s(0))
lesscC_in_gg(s(X1), s(X2)) → U26_gg(X1, X2, lesscC_in_gg(X1, X2))
U26_gg(X1, X2, lesscC_out_gg(X1, X2)) → lesscC_out_gg(s(X1), s(X2))
LESSC_IN_GG(s(X1), s(X2)) → LESSC_IN_GG(X1, X2)
leqcB_in_gg(0, 0) → leqcB_out_gg(0, 0)
leqcB_in_gg(0, s(0)) → leqcB_out_gg(0, s(0))
leqcB_in_gg(s(X1), s(X2)) → U25_gg(X1, X2, leqcB_in_gg(X1, X2))
U25_gg(X1, X2, leqcB_out_gg(X1, X2)) → leqcB_out_gg(s(X1), s(X2))
lesscC_in_gg(0, s(0)) → lesscC_out_gg(0, s(0))
lesscC_in_gg(s(X1), s(X2)) → U26_gg(X1, X2, lesscC_in_gg(X1, X2))
U26_gg(X1, X2, lesscC_out_gg(X1, X2)) → lesscC_out_gg(s(X1), s(X2))
LESSC_IN_GG(s(X1), s(X2)) → LESSC_IN_GG(X1, X2)
LESSC_IN_GG(s(X1), s(X2)) → LESSC_IN_GG(X1, X2)
From the DPs we obtained the following set of size-change graphs:
LEQB_IN_GG(s(X1), s(X2)) → LEQB_IN_GG(X1, X2)
leqcB_in_gg(0, 0) → leqcB_out_gg(0, 0)
leqcB_in_gg(0, s(0)) → leqcB_out_gg(0, s(0))
leqcB_in_gg(s(X1), s(X2)) → U25_gg(X1, X2, leqcB_in_gg(X1, X2))
U25_gg(X1, X2, leqcB_out_gg(X1, X2)) → leqcB_out_gg(s(X1), s(X2))
lesscC_in_gg(0, s(0)) → lesscC_out_gg(0, s(0))
lesscC_in_gg(s(X1), s(X2)) → U26_gg(X1, X2, lesscC_in_gg(X1, X2))
U26_gg(X1, X2, lesscC_out_gg(X1, X2)) → lesscC_out_gg(s(X1), s(X2))
LEQB_IN_GG(s(X1), s(X2)) → LEQB_IN_GG(X1, X2)
LEQB_IN_GG(s(X1), s(X2)) → LEQB_IN_GG(X1, X2)
From the DPs we obtained the following set of size-change graphs:
MERGEA_IN_GGA(.(X1, X2), .(X3, X4), .(X3, X5)) → U9_GGA(X1, X2, X3, X4, X5, lesscC_in_gg(X3, X1))
U9_GGA(X1, X2, X3, X4, X5, lesscC_out_gg(X3, X1)) → MERGEA_IN_GGA(.(X1, X2), X4, X5)
MERGEA_IN_GGA(.(0, X1), .(0, X2), .(0, X3)) → MERGEA_IN_GGA(X1, .(0, X2), X3)
MERGEA_IN_GGA(.(s(0), X1), .(0, X2), .(0, X3)) → MERGEA_IN_GGA(.(s(0), X1), X2, X3)
MERGEA_IN_GGA(.(s(X1), X2), .(s(X3), X4), .(s(X1), X5)) → U6_GGA(X1, X2, X3, X4, X5, leqcB_in_gg(X1, X3))
U6_GGA(X1, X2, X3, X4, X5, leqcB_out_gg(X1, X3)) → MERGEA_IN_GGA(X2, .(s(X3), X4), X5)
MERGEA_IN_GGA(.(0, X1), .(s(0), X2), .(0, X3)) → MERGEA_IN_GGA(X1, .(s(0), X2), X3)
MERGEA_IN_GGA(.(s(X1), X2), .(s(X3), X4), .(s(X3), X5)) → U13_GGA(X1, X2, X3, X4, X5, lesscC_in_gg(X3, X1))
U13_GGA(X1, X2, X3, X4, X5, lesscC_out_gg(X3, X1)) → MERGEA_IN_GGA(.(s(X1), X2), X4, X5)
leqcB_in_gg(0, 0) → leqcB_out_gg(0, 0)
leqcB_in_gg(0, s(0)) → leqcB_out_gg(0, s(0))
leqcB_in_gg(s(X1), s(X2)) → U25_gg(X1, X2, leqcB_in_gg(X1, X2))
U25_gg(X1, X2, leqcB_out_gg(X1, X2)) → leqcB_out_gg(s(X1), s(X2))
lesscC_in_gg(0, s(0)) → lesscC_out_gg(0, s(0))
lesscC_in_gg(s(X1), s(X2)) → U26_gg(X1, X2, lesscC_in_gg(X1, X2))
U26_gg(X1, X2, lesscC_out_gg(X1, X2)) → lesscC_out_gg(s(X1), s(X2))
MERGEA_IN_GGA(.(X1, X2), .(X3, X4)) → U9_GGA(X1, X2, X3, X4, lesscC_in_gg(X3, X1))
U9_GGA(X1, X2, X3, X4, lesscC_out_gg(X3, X1)) → MERGEA_IN_GGA(.(X1, X2), X4)
MERGEA_IN_GGA(.(0, X1), .(0, X2)) → MERGEA_IN_GGA(X1, .(0, X2))
MERGEA_IN_GGA(.(s(0), X1), .(0, X2)) → MERGEA_IN_GGA(.(s(0), X1), X2)
MERGEA_IN_GGA(.(s(X1), X2), .(s(X3), X4)) → U6_GGA(X1, X2, X3, X4, leqcB_in_gg(X1, X3))
U6_GGA(X1, X2, X3, X4, leqcB_out_gg(X1, X3)) → MERGEA_IN_GGA(X2, .(s(X3), X4))
MERGEA_IN_GGA(.(0, X1), .(s(0), X2)) → MERGEA_IN_GGA(X1, .(s(0), X2))
MERGEA_IN_GGA(.(s(X1), X2), .(s(X3), X4)) → U13_GGA(X1, X2, X3, X4, lesscC_in_gg(X3, X1))
U13_GGA(X1, X2, X3, X4, lesscC_out_gg(X3, X1)) → MERGEA_IN_GGA(.(s(X1), X2), X4)
leqcB_in_gg(0, 0) → leqcB_out_gg(0, 0)
leqcB_in_gg(0, s(0)) → leqcB_out_gg(0, s(0))
leqcB_in_gg(s(X1), s(X2)) → U25_gg(X1, X2, leqcB_in_gg(X1, X2))
U25_gg(X1, X2, leqcB_out_gg(X1, X2)) → leqcB_out_gg(s(X1), s(X2))
lesscC_in_gg(0, s(0)) → lesscC_out_gg(0, s(0))
lesscC_in_gg(s(X1), s(X2)) → U26_gg(X1, X2, lesscC_in_gg(X1, X2))
U26_gg(X1, X2, lesscC_out_gg(X1, X2)) → lesscC_out_gg(s(X1), s(X2))
leqcB_in_gg(x0, x1)
U25_gg(x0, x1, x2)
lesscC_in_gg(x0, x1)
U26_gg(x0, x1, x2)
MERGEA_IN_GGA(.(X1, X2), .(X3, X4)) → U9_GGA(X1, X2, X3, X4, lesscC_in_gg(X3, X1))
MERGEA_IN_GGA(.(0, X1), .(0, X2)) → MERGEA_IN_GGA(X1, .(0, X2))
MERGEA_IN_GGA(.(s(0), X1), .(0, X2)) → MERGEA_IN_GGA(.(s(0), X1), X2)
MERGEA_IN_GGA(.(s(X1), X2), .(s(X3), X4)) → U6_GGA(X1, X2, X3, X4, leqcB_in_gg(X1, X3))
U6_GGA(X1, X2, X3, X4, leqcB_out_gg(X1, X3)) → MERGEA_IN_GGA(X2, .(s(X3), X4))
MERGEA_IN_GGA(.(0, X1), .(s(0), X2)) → MERGEA_IN_GGA(X1, .(s(0), X2))
MERGEA_IN_GGA(.(s(X1), X2), .(s(X3), X4)) → U13_GGA(X1, X2, X3, X4, lesscC_in_gg(X3, X1))
U13_GGA(X1, X2, X3, X4, lesscC_out_gg(X3, X1)) → MERGEA_IN_GGA(.(s(X1), X2), X4)
POL(.(x1, x2)) = 2 + x1 + x2
POL(0) = 0
POL(MERGEA_IN_GGA(x1, x2)) = 2·x1 + 2·x2
POL(U13_GGA(x1, x2, x3, x4, x5)) = 1 + 2·x1 + 2·x2 + 2·x3 + 2·x4 + 2·x5
POL(U25_gg(x1, x2, x3)) = x1 + x2 + x3
POL(U26_gg(x1, x2, x3)) = x1 + x2 + x3
POL(U6_GGA(x1, x2, x3, x4, x5)) = 1 + 2·x1 + 2·x2 + 2·x3 + 2·x4 + 2·x5
POL(U9_GGA(x1, x2, x3, x4, x5)) = 2 + x1 + 2·x2 + x3 + 2·x4 + x5
POL(leqcB_in_gg(x1, x2)) = 2 + x1 + x2
POL(leqcB_out_gg(x1, x2)) = 2 + x1 + x2
POL(lesscC_in_gg(x1, x2)) = 2 + x1 + x2
POL(lesscC_out_gg(x1, x2)) = 2 + x1 + x2
POL(s(x1)) = 2·x1
U9_GGA(X1, X2, X3, X4, lesscC_out_gg(X3, X1)) → MERGEA_IN_GGA(.(X1, X2), X4)
leqcB_in_gg(0, 0) → leqcB_out_gg(0, 0)
leqcB_in_gg(0, s(0)) → leqcB_out_gg(0, s(0))
leqcB_in_gg(s(X1), s(X2)) → U25_gg(X1, X2, leqcB_in_gg(X1, X2))
U25_gg(X1, X2, leqcB_out_gg(X1, X2)) → leqcB_out_gg(s(X1), s(X2))
lesscC_in_gg(0, s(0)) → lesscC_out_gg(0, s(0))
lesscC_in_gg(s(X1), s(X2)) → U26_gg(X1, X2, lesscC_in_gg(X1, X2))
U26_gg(X1, X2, lesscC_out_gg(X1, X2)) → lesscC_out_gg(s(X1), s(X2))
leqcB_in_gg(x0, x1)
U25_gg(x0, x1, x2)
lesscC_in_gg(x0, x1)
U26_gg(x0, x1, x2)